|
In mathematical logic, given an unsatisfiable Boolean propositional formula in conjunctive normal form, a subset of clauses whose conjunction is still unsatisfiable is called an unsatisfiable core of the original formula. Many SAT solvers can produce a ''resolution graph'' which proves the unsatisfiability of the original problem. This can be analyzed to produce a smaller unsatisfiable core. An unsatisfiable core is called a ''minimal unsatisfiable core'', if every proper subset (allowing removal of any arbitrary clause or clauses) of it is satisfiable. Thus, such a core is a local minimum, though not necessarily a global one. There are several practical methods of computing minimal unsatisfiable cores.〔N. Dershowitz, Z. Hanna, and A. Nadel, ( A Scalable Algorithm for Minimal Unsatisfiable Core Extraction )〕〔Stefan Szeider, (Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable )〕 A ''minimum unsatisfiable core'' contains the smallest number of the original clauses required to still be unsatisfiable. No practical algorithms for computing the minimum core are known. (Algorithms for Computing Minimal Unsatisfiable Subsets ). Notice the terminology: whereas ''minimal unsatisfiable core'' was a local problem with an easy solution, the ''minimum unsatisfiable core'' is a global problem with no known easy solution. == References == 〔 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Unsatisfiable core」の詳細全文を読む スポンサード リンク
|